(set-logic ALL)
(define-fun s1 () Int 10)
(define-fun s3 () Int 0)
(define-fun s7 () Int 1)
(define-fun s11 () Int 32)
(define-fun s12 () Int 18)
(define-fun s21 () Int 5)
(declare-fun s0 () Int)
(define-fun s2 () Int (mod s0 s1))
(define-fun s4 () Bool (>= s0 s3))
(define-fun s5 () Bool (= s2 s3))
(define-fun s6 () Bool (or s4 s5))
(define-fun s8 () Int (ite s6 s3 s7))
(define-fun s9 () Int (* s1 s8))
(define-fun s10 () Int (- s2 s9))
(define-fun s13 () Int (* s0 s12))
(define-fun s14 () Int (mod s13 s1))
(define-fun s15 () Bool (>= s13 s3))
(define-fun s16 () Bool (= s3 s14))
(define-fun s17 () Bool (or s15 s16))
(define-fun s18 () Int (ite s17 s3 s7))
(define-fun s19 () Int (* s1 s18))
(define-fun s20 () Int (- s14 s19))
(define-fun s22 () Bool (>= s20 s21))
(define-fun s23 () Int (div s13 s1))
(define-fun s24 () Int (+ s18 s23))
(define-fun s25 () Int (+ s7 s24))
(define-fun s26 () Int (ite s22 s25 s24))
(define-fun s27 () Int (+ s11 s26))
(define-fun s28 () Int (div s27 s1))
(define-fun s29 () Bool (>= s27 s3))
(define-fun s30 () Int (mod s27 s1))
(define-fun s31 () Bool (= s3 s30))
(define-fun s32 () Bool (or s29 s31))
(define-fun s33 () Int (ite s32 s3 s7))
(define-fun s34 () Int (+ s28 s33))
(define-fun s35 () Bool (= s10 s34))
(define-fun s36 () Int (div s0 s1))
(define-fun s37 () Int (+ s8 s36))
(define-fun s38 () Int (* s1 s33))
(define-fun s39 () Int (- s30 s38))
(define-fun s40 () Bool (= s37 s39))
(define-fun s41 () Bool (and s35 s40))
(assert s41)
(check-sat)
